case x1 of 
Rnone => none
Rplus(left,right)=>rec1,rec2.plus(left;right;rec1;rec2)
Rinit(loc,T,x,v)=> init(loc;T;x;v)
Rframe(loc,T,x,L)=> frame(loc;T;x;L)
Rsframe(lnk,tag,L)=> sframe(lnk;tag;L)
Reffect(loc,ds,knd,T,x,f)=> effect(loc;ds;knd;T;x;f)
Rsends(ds,knd,T,l,dt,g)=> sends(ds;knd;T;l;dt;g)
Rpre(loc,ds,a,T,P)=> pre(loc;ds;a;T;P)
Raframe(loc,k,L)=> aframe(loc;k;L)
Rbframe(loc,k,L)=> bframe(loc;k;L)
Rrframe(loc,x,L)=> rframe(loc;x;L)
== Case x1 of
== inl(x)  none
== inr(x)  Case x of
== inr(x)  inl(x)  plus(1of(x)
== inr(x)  inl(x)  plus;2of(x)
== inr(x)  inl(x)  plus;case 1of(x) of 
== inr(x)  inl(x)  plus;Rnone => none
== inr(x)  inl(x)  plus;Rplus(left,right)=>rec1,rec2.plus(left;right;rec1;rec2)
== inr(x)  inl(x)  plus;Rinit(loc,T,x,v)=> init(loc;T;x;v)
== inr(x)  inl(x)  plus;Rframe(loc,T,x,L)=> frame(loc;T;x;L)
== inr(x)  inl(x)  plus;Rsframe(lnk,tag,L)=> sframe(lnk;tag;L)
== inr(x)  inl(x)  plus;Reffect(loc,ds,knd,T,x,f)=> effect(loc;ds;knd;T;x;f)
== inr(x)  inl(x)  plus;Rsends(ds,knd,T,l,dt,g)=> sends(ds;knd;T;l;dt;g)
== inr(x)  inl(x)  plus;Rpre(loc,ds,a,T,P)=> pre(loc;ds;a;T;P)
== inr(x)  inl(x)  plus;Raframe(loc,k,L)=> aframe(loc;k;L)
== inr(x)  inl(x)  plus;Rbframe(loc,k,L)=> bframe(loc;k;L)
== inr(x)  inl(x)  plus;Rrframe(loc,x,L)=> rframe(loc;x;L)
== inr(x)  inl(x)  plus;case 2of(x) of 
== inr(x)  inl(x)  plus;Rnone => none
== inr(x)  inl(x)  plus;Rplus(left,right)=>rec1,rec2.plus(left;right;rec1;rec2)
== inr(x)  inl(x)  plus;Rinit(loc,T,x,v)=> init(loc;T;x;v)
== inr(x)  inl(x)  plus;Rframe(loc,T,x,L)=> frame(loc;T;x;L)
== inr(x)  inl(x)  plus;Rsframe(lnk,tag,L)=> sframe(lnk;tag;L)
== inr(x)  inl(x)  plus;Reffect(loc,ds,knd,T,x,f)=> effect(loc;ds;knd;T;x;f)
== inr(x)  inl(x)  plus;Rsends(ds,knd,T,l,dt,g)=> sends(ds;knd;T;l;dt;g)
== inr(x)  inl(x)  plus;Rpre(loc,ds,a,T,P)=> pre(loc;ds;a;T;P)
== inr(x)  inl(x)  plus;Raframe(loc,k,L)=> aframe(loc;k;L)
== inr(x)  inl(x)  plus;Rbframe(loc,k,L)=> bframe(loc;k;L)
== inr(x)  inl(x)  plus;Rrframe(loc,x,L)=> rframe(loc;x;L))
== inr(x)  inr(x)  Case x of
== inr(x)  inr(x)  inl(x)  init(1of(x);1of(2of(x));1of(2of(2of(x)));2of(2of(2of(x))))
== inr(x)  inr(x)  inr(x)  Case x of
== inr(x)  inr(x)  inr(x)  inl(x)  frame(1of(x);1of(2of(x));1of(2of(2of(x)));2of(2of(2of(x))))
== inr(x)  inr(x)  inr(x)  inr(x)  Case x of
== inr(x)  inr(x)  inr(x)  inr(x)  inl(x)  sframe(1of(x);1of(2of(x));2of(2of(x)))
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  Case x of
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inl(x)  effect(1of(x)
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inl(x)  effect;1of(2of(x))
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inl(x)  effect;1of(2of(2of(x)))
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inl(x)  effect;1of(2of(2of(2of(x))))
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inl(x)  effect;1of(2of(2of(2of(2of(x)))))
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inl(x)  effect;2of(2of(2of(2of(2of(x))))))
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  Case x of
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inl(x)  sends(1of(x)
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inl(x)  sends;1of(2of(x))
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inl(x)  sends;1of(2of(2of(x)))
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inl(x)  sends;1of(2of(2of(2of(x))))
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inl(x)  sends;1of(2of(2of(2of(2of(x)))))
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inl(x)  sends;2of(2of(2of(2of(2of(x))))))
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  Case x of
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inl(x)  pre(1of(x)
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inl(x)  pre;1of(2of(x))
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inl(x)  pre;1of(2of(2of(x)))
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inl(x)  pre;1of(2of(2of(2of(x))))
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inl(x)  pre;2of(2of(2of(2of(
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inl(x)  pre;x)))))
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  Case x of
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inl(x)  aframe(1of(x)
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inl(x)  aframe;1of(2of(
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inl(x)  aframe;1of(x))
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inl(x)  aframe;2of(2of(
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inl(x)  aframe;x)))
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  Case x of
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inl(x)
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)   bframe(1of(x)
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)   bframe;1of(
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)   bframe;2of(x))
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)   bframe;2of(
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)   bframe;2of(
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)   bframe;x)))
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)   rframe(1of(x)
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)   rframe;1of(
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)   rframe;2of(x))
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)   rframe;2of(
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)   rframe;2of(
== inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)  inr(x)   rframe;x)))
(recursive) 

latex

Definitions	Y, x.A(x), f(a), Case b of inl(x)  s(x) ; inr(y)  t(y), 1of(t), 2of(t)
FDL editor aliases	es_realizer_ind